T:Type, L1, L2:T List, x, y:T. L1  L2  x before y  L1  x before y  L2 

latex

Definitions	x:A. B(x), l1  l2, x:A. B(x), L1  L2, P  Q, t  T, Prop, ||as||, ij, False, A, AB, , {T}, SQType(T), P & Q, P  Q, as @ bs, x before y  l
Lemmas	append wf, le wf, cons one one, nat wf, non neg length, length wf1, sublist wf, member wf, sublist transitivity, sublist weakening, interleaving sublist, sublist iseg, sublist append1